/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.ast;

import java.util.Iterator;

import alloy.util.Dbg;

public class Decl extends TreeNode {

    /**
     * true if empty
     */
    private boolean _empty = false;

    /**
     * index of expr in child list
     */
    private static final int EXPR_INDEX = 1;

    /**
     * index of variables in child list
     */
    private static final int VARIABLES_INDEX = 0;

    /**
     * true if variables declared are disjoint
     */
    private boolean _isDisj = false;

    /**
     * true if variables declared are exhaustive
     */
    private boolean _isExh = false;

    /**
     * true if this declaration has been desugared, i.e. the
     * constraints implied by this have already been generated
     */
    public boolean desugared = false;

    public Decl() {
        super(Location.UNKNOWN);
        _empty = true;
    }

    public Decl(Location location_, Qualifiers qualifiers_, Variables variables_, MultiplicityExpr expr_) {
        super(location_, variables_, expr_);
        // set disj and exh booleans appropriately given qualifiers
        Iterator qualIter = qualifiers_.getQualifierIter();
        while (qualIter.hasNext()) {
            Qualifier qualifier = (Qualifier)qualIter.next();
            if(qualifier.equals(Qualifier.PART)){
                _isDisj = true;
                _isExh = true;
            } else if(qualifier.equals(Qualifier.DISJ)){
                _isDisj = true;
            } else if(qualifier.equals(Qualifier.EXH)) {
                _isExh = true;
            }
        }
    }


    public Decl(Qualifiers qualifiers_, Variables variables_, MultiplicityExpr expr_) {
        this(Location.UNKNOWN, qualifiers_, variables_, expr_);
    }


    /**
     * @return true if this is empty
     */
    public boolean isEmpty() {
        return _empty;
    }

    //GET AND SET METHODS

    /**
     * gets the expr of this
     * @return the {@link MultiplicityExpr}
     */
    public MultiplicityExpr getExpr() {
    Dbg.chk(!_empty, "attempt to use empty decl");
        return (MultiplicityExpr)childAt(EXPR_INDEX);
    }

    public void setExpr(MultiplicityExpr multExpr_) {
        setChild(EXPR_INDEX, multExpr_);
    }

    public boolean isDisj() {
        return _isDisj;
    }

    public boolean isExh() {
        return _isExh;
    }

    /**
     * gets the variables of this
     * @return the {@link Variables}
     */
    public Variables getVariables() {
    Dbg.chk(!_empty, "attempt to use empty decl");
        return (Variables)childAt(VARIABLES_INDEX);
    }

    /**
       @return <code>true</code> if this is higher-order, <code>false</code>
       otherwise
    */
    public boolean isHigherOrder() {
    Dbg.chk(!_empty, "attempt to use empty decl");
        boolean ret = false;
        MultiplicityExpr multExpr = getExpr();
        if (multExpr instanceof ArrowMultExpr) {
            ret = true;
        } else {
            SetMultExpr setMultExpr = (SetMultExpr)multExpr;
            // must have 1 basic type and multiplcity scalar
            if (setMultExpr.getType().arity() != 1) ret = true;
            Multiplicity mult = setMultExpr.getMult();
            if (mult.equals(Multiplicity.SET) || mult.equals(Multiplicity.LONE) ||
                    mult.equals(Multiplicity.SOME))
                ret = true;
        }
        return ret;
    }

    /**
     * accept an AST visitor
     * @param visitor_ the visitor
     */
    protected void acceptVisitor(ASTVisitor visitor_) {
        visitor_.visit(this);
    }

    /**
     * accept a returning AST visitor
     * @param visitor_ the visitor
     * @return the Object returned by the visitor
     */
    protected Object acceptReturnVisitor(ASTReturnVisitor visitor_) {
        return visitor_.visit(this);
    }

    public String nodeString() {
        String ret = "";
        if (!_empty) {
            ret = getVariables().nodeString() + " : " + getExpr().nodeString();
        }
        return ret;
    }

    public String toString()
    {
        return nodeString();
    }

    /** @return copy of decl with desugared flag set to false */
    public final Object copy() {
        Decl copy = (Decl)super.copy();
        copy.desugared = false;
        return copy;
    }

    /** creates typical Decl used when desugaring formulas, adding
        constraints, etc. */
    public static Decl in(Variable var_, MultiplicityExpr expr_) {
        Variables vars = new Variables();
        vars.addVariable(var_);
        return new Decl(new Qualifiers(), vars, expr_);
    }
}



















